上一篇整理了漏洞的分類，接下來就要開始實際檢查合約了。在跑工具以前，先介紹主要使用到的幾個智慧合約審計工具和一個資料集。
這三個工具會交出不同的東西：Slither 會給警示 (Finding)，Foundry 測試失敗時會給反例 (Counterexample)，Certora 則會告訴我們某條規則通過或失敗，規則通過就是證明 (Proof)。三個工具的運作方式完全不同，回答「可能有漏洞嗎」的方式也不一樣，下面一一介紹。
Slither 是 Trail of Bits 開發的靜態分析 (Static Analysis) 工具。它不需要真的執行合約，會先編譯 Solidity，再依照偵測器 (Detectors) 在程式碼裡尋找特定模式，並產生警示。
警示可能是真的漏洞，也可能是誤報，還是要透過其他方式確認。沒有警示，也只是偵測器沒找到認得的漏洞模式，程式裡還是可能有別的問題。
Foundry 是智慧合約的開發與測試框架，測試可以直接用 Solidity 寫。除了一般的單元測試 (Unit Testing)，還有模糊測試 (Fuzz Testing) 跟不變量測試 (Invariant Testing)，也可以 fork 某條鏈的歷史區塊，用當時的鏈上狀態跑測試。
模糊測試會自動產生大量輸入，不變量測試則會隨機串起一連串操作。測試裡會寫好斷言 (assertion)，也就是「跑完之後這件事必須成立」的檢查。只要有一次斷言失敗，Foundry 就會把那組輸入或操作順序留下來當作反例，之後可以拿來重跑。
測試全部通過的話，只代表這次跑到的輸入沒出問題。就算跑一萬次，也還是會有沒跑到的狀態。
Certora Prover 是形式化驗證 (Formal Verification) 工具。要先用 CVL (Certora Verification Language) 把「合約應該滿足什麼」寫成規則，Certora 再把合約和規則轉成邏輯條件，交給求解器 (SMT solver) 去找有沒有讓規則失敗的狀態。找到就回傳反例，找不到規則才算通過。
規則通過，也只是在目前的模型和假設下成立。如果規則漏寫了條件、require 限制得太嚴，或外部合約沒有被建模，這些都不在證明的範圍裡。
DeFiHackLabs 是一個開源專案，把過去真實發生的 DeFi 攻擊事件，用 Foundry 寫成可以執行的概念驗證程式 (PoC)。這個系列的案例都會從這裡挑。
這些 PoC 會 fork 特定鏈的歷史區塊，在攻擊發生當下的鏈上狀態裡重演整起事件。後面的文章會從案例裡抽出造成漏洞的那段合約，做成最小版本，再拿去給三個工具檢查。
| 工具 | 分析方式 | 輸出 | 限制 |
|---|---|---|---|
| Slither | 靜態分析 | 警示 | 沒有警示不代表沒有問題 |
| Foundry | 動態測試 (模糊測試、不變量測試) | 可重跑的反例 | 只涵蓋這次跑到的輸入 |
| Certora | 形式化驗證 | 規則通過或反例 | 只在目前的模型與假設下成立 |
將拆解一個真實的漏洞範例。
iThome鐵人賽
看影片追技術